Section: Partnerships and Cooperations

National Initiatives

Inria Large Scale Actions

Inria Large Scale Action Synchronics : Language Platform for Embedded System Design

Participants : Gwenaël Delaval, Alain Girault [contact person, co-coordinator] , Bertrand Jeannet, Xavier Nicollin, Peter Schrammel.

The Synchronics (Language Platform for Embedded System Design) project [mid-2008 to mid-2012] gathers 9 permanent researchers on the topic of embedded systems design: B. Caillaud (Inria Rennes – Bretagne Atlantique), A. Cohen, L. Mandel, and M. Pouzet (Inria-Saclay and ENS Paris), G. Delaval, A. Girault, and B. Jeannet (Inria Grenoble – Rhône-Alpes), E. Jahier and P. Raymond (VERIMAG).

Synchronics capitalizes on recent extensions of data-flow synchronous languages, as well as relaxed forms of synchronous composition or compilation techniques for various platform, to address two main challenges with a language-centered approach: (i) the co-simulation of mixed discrete-continuous specifications, and more generally the co-simulation of programs and properties (either discrete or continuous); (ii) the ability, inside the programming model, to account for the architecture constraints (execution time, memory footprint, energy, power, reliability, etc.).

ANR

ANR Asopt : Analyse Statique et OPTimisation

Participants : Bertrand Jeannet [contact person, coordinator] , Peter Schrammel.

The Asopt (Analyse Statique et OPTimisation) project [january 2009-july 2012] (http://asopt.inrialpes.fr/index.php ) brings together static analysis (Inria-Pop Art , VERIMAG, CEA LMeASI), optimisation, and control/game theory experts (CEA LMeASI, Inria-MAXPLUS) around some program verification problems. Pop Art is the project coordinator.

Many abstract interpretations attempt to find “good” geometric shapes verifying certain constraints; this not only applies to purely numerical abstractions (for numerical program variables), but also to abstractions of data structures (arrays and more complex shapes). This problem can often be addressed by optimisation techniques, opening the possibility of exploiting advanced techniques from mathematical programming.

The purpose of Asopt is to develop new abstract domains and new resolution techniques for embedded control programs, and in the longer run, for numerical simulation programs.

The main results are 1. improved numerical abstract domains (in particular the MaxPLus polyhedra and zonotopes-based abstract domains), and their combination with finite-types domains (using BDDs); 2. new symbolic domains, in particular for the accurate analysis of aliased expressions in data-structures and for precise interprocedural analysis in the presence of pointers to the call-stack; 3. improved equation solving techniques, with the generalization of the policy iteration approach and the widening of its applicability; 4. precise abstractions of full blocks of code, based either on quantifier elimination or on abstract acceleration.

Most of these contributions have been integrated into either the Fixpoint library or the Apron /BddApron libraries and they can be experimented on-line or off-line with the Interproc analyzer (see Section  5.5.5 ), which was the common experimental platform of the project.

ANR Vedecy : Verification and Design of Cyber-physical Systems

Participants : Gregor Goessler [contact person] , Bertrand Jeannet, Sebti Mouelhi.

The Vedecy project brings together hybrid systems and formal methods experts. Three partners are involved: Laboratoire Jean Kuntzmann (LJK), Inria Pop Art , and VERIMAG.

Vedecy aims at pursuing fundamental research towards the development of algorithmic approaches to the verification and design of cyber-physical systems. Cyber-physical systems result from the integration of computations with physical processes: embedded computers control physical processes which in return affect computations through feedback loops. They are ubiquitous in current technology and their impact on lives of citizens is meant to grow in the future (autonomous vehicles, robotic surgery, energy efficient buildings, ...).

Cyber-physical systems applications are often safety critical and therefore reliability is a major requirement. To provide assurance of reliability, model based approaches and formal methods are appealing. Models of cyber-physical systems are heterogeneous by nature: discrete dynamic systems for computations and continuous differential equations for physical processes. The theory of hybrid systems offers a sound modeling framework for cyber-physical systems. The purpose of Vedecy is to develop hybrid systems techniques for the verification and the design of cyber-physical systems.